#include "dpll_openmp.h"
#include "timer.h"

extern timer tm;
static int numtask = 0;
extern int CERR_LEVELS[]; 
_bool stop, openmpbreak;
extern long long threshold;
static dpllresult* DPLLalgorithm_omp(cnf* cnf);

pthread_mutex_t oricnf_m;
static void set_variable_value3(cnf* cnf, variable* var, _bool value){
    assert(sizeof(variable) == sizeof(int));//security check
    int name = var->name;
    //timer_start(&tm);
#ifdef __serial
    for(int i = 0; i < cnf->nvar; i++){
        if(name == cnf->vars[i].name){
            cnf->vars[i].assigned = true;
            cnf->vars[i].value = value;
            //printf("index %d, set flag to %d\n", i,  cnf->vars[i].flag);
        }
    }
    for(int i = 0; i < cnf->n_univar; i++){
        if (name == cnf->var_set[i].name){
            cnf->var_set[i].assigned = true;
            cnf->var_set[i].value = value;
        }
    }
#endif 
#ifdef __vector
    TODO();
#endif
}
void print_vars(variable* vars, int n);

static void unset_variable_value3(cnf* cnf, variable* var){
    for(int i = 0; i < cnf->nvar; i++){
        if(var->name == cnf->vars[i].name){
            cnf->vars[i].assigned = false;
        }   
    }
    for(int i = 0; i < cnf->n_univar; i++){
        if(var->name== cnf->var_set[i].name){
            cnf->var_set[i].assigned = false;
            break;
        }
    }
}


_bool dpll_satisfiable_omp(cnf* _cnf){
    printf("start new task\n");
    dpllresult* result = DPLLalgorithm_omp(_cnf);
    if (result == NULL) return false;
    if (result->sat && result->model_cnf != NULL){
        openmpbreak = true;     //设置让剩余的openmp task空转
        _cnf = new_cnf_from(result->model_cnf);
        print_cnf(_cnf);
    }
    return result->sat;
}

extern list_entry_t task_list;
dpll_task_t* new_task(variable* var_set, int n_univar);
void free_task(dpll_task_t* task);

static void init_tasklist(cnf* cnf){
    list_init(&task_list); //初始化表格

    //建立第一条任务
    printf("first task inited\n");
    dpll_task_t* firsttask = new_task(cnf->var_set, cnf->n_univar); 

    list_add_after(&task_list, &firsttask->entry);  //  插入列表
    numtask++;
}
static void task_reload(cnf* cnf, dpll_task_t* task);
int i = 0;
dpll_task_t* tasks[10*MAX_TOTTASK+20];

static void add_enough_task(cnf* const cnf1){
    if (CERR_LEVELS[0] > MAX_TASK_CEER) {
        tasks[i++] = new_task(cnf1->var_set, cnf1->n_univar); 
      //  printf("add new task %d\n", i);
        return;
    }
    //printf("add enough task %d\n", CERR_LEVELS[0]);

    if (CERR_LEVELS[0] <= MAX_TASK_CEER){
        //add new tasks
        variable* var = find_first_unassigned(cnf1->vars, cnf1->nvar);
        if(var == NULL){
            printf("maybe too less variables totally or inner error\n");
            exit(0); 
        }
        struct _cnf * copycnf, *copycnf2;
        copycnf = new_cnf_from(cnf1);
        copycnf2 = new_cnf_from(cnf1);
        set_variable_value3(copycnf, var, true);        
        //print_cnf(copycnf);
        //printf("#1 level %d\n", CERR_LEVELS[0]);

        CERR_LEVELS[0]++;
        add_enough_task(copycnf);
        CERR_LEVELS[0]--;
        delete_cnf(copycnf);
        //printf("#2 level %d\n", CERR_LEVELS[0]);

        set_variable_value3(copycnf2, var, false);
        CERR_LEVELS[0]++;
        add_enough_task(copycnf2);
        CERR_LEVELS[0]--;
        delete_cnf(copycnf2);

        //print_cnf(cnf);
        //printf("finish level %d\n", CERR_LEVELS[0]);

    }
    else{
        printf("inner error\n");
        exit(0);
    }
}


static void task_reload(cnf* cnf, dpll_task_t* task){
    //we guaruntee that every cnf is blocked when copy, 
    //so change on single variable will go over all cnf->vars
    //which means we don't need to check all of them
    //printf("reload\n");
    variable* taskvarset = task->vars_set;
    int n_univar = task->n_univar;
    if(n_univar != cnf->n_univar){
        printf("inner error n_univar %d %d, %p\n", n_univar, cnf->n_univar, task);
        exit(0);
    }else{
        //printf("ok n_univar %d %d, %p\n", n_univar, cnf->n_univar, task);
    }

    //print_vars(task->vars_set, task->n_univar);

    for(int i = 0; i < n_univar; i++){
        if(taskvarset[i].name != cnf->var_set[i].name) {
            printf("inner error 2\n");
            exit(0);
        }
        if(!taskvarset[i].assigned && cnf->var_set[i].assigned){
            unset_variable_value3(cnf, &taskvarset[i]);
        }
        if(taskvarset[i].assigned){
            set_variable_value3(cnf, &taskvarset[i], taskvarset[i].value);
        }
    }
    //printf("[thread %d]LOADED IN\n", threadid);
    //print_cnf(cnf);
    // if(threshold > 1)exit(0);
    //printf("task reload fine\n");
}
void print_vars(variable* vars, int n);

cnf* global_init_cnf;
static dpllresult* DPLLalgo_omp(cnf* cnf1 , dpll_task_t* task1){
    //printf(" DPLLalgo_omp task:%p\n", task);
    //print_vars(task->vars_set, task->n_univar);    
    //print_cnf(global_init_cnf);
    //exit(0);
    if (cnf1 == NULL){
        printf("init cnfl\n");
        exit(0);    
    }

    task_reload(cnf1, task1);
    return DPLLalgorithm(cnf1);
}
dpllresult* finalresult;
static void run_omp(){
    dpllresult* result = NULL;
    cnf* ompcnf = NULL;
    dpll_task_t* task;
    print_cnf(global_init_cnf);
    printf("start %d\n", numtask);

    #pragma omp parallel for private(result) private(task) private(ompcnf) num_threads(OMP_THREADNUM)
    for(int i = 0; i < numtask; i++){        
        //if (i == 1045) continue;
        
        ompcnf = new_cnf_from(global_init_cnf);
        

        task = tasks[i];
            
        task_reload(ompcnf, task);
        result = DPLLalgorithm(ompcnf);
        // #pragma omp critical
        // {
        //     task_reload(ompcnf, task);
        //     result = DPLLalgorithm(ompcnf);
        // }
        
        //result = DPLLalgo_omp(ompcnf, task);
        if(result && result->sat) {
            finalresult = result;}
        // }#pragma omp critical
        // {
            
        // }
        
    }

    printf("finished\n");
}

static dpllresult* DPLLalgorithm_omp(cnf* cnf){
    global_init_cnf = new_cnf_from(cnf);
    //exit(0);
    init_tasklist(cnf);
    CERR_LEVELS[0] = 0;
    void* test1 = global_init_cnf;
    print_cnf(global_init_cnf);


    add_enough_task(global_init_cnf);
    numtask= i;
    for(int j = 1; j < numtask; j++){
        if(tasks[j]->n_univar != tasks[0]->n_univar){
            printf("task %d n_univar error\n", j);
            exit(0);
        }else{
            printf("%d %p\n", j, tasks[j]);
        }
    }
    //exit(0);
    //get_task_list();
    //return NULL;.
    if(global_init_cnf != test1) {
        printf("%p %p, ??\n", global_init_cnf, test1);
        global_init_cnf = new_cnf_from(test1);
    }

    run_omp();

    return finalresult;
}

